package br.cin.ufpe.rabbit;

import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.jvm.ClassInfo;
import gov.nasa.jpf.jvm.ElementInfo;
import gov.nasa.jpf.jvm.JVM;
import gov.nasa.jpf.jvm.MethodInfo;
import gov.nasa.jpf.jvm.StackFrame;
import gov.nasa.jpf.jvm.ThreadInfo;
import gov.nasa.jpf.jvm.bytecode.INVOKESPECIAL;
import gov.nasa.jpf.jvm.bytecode.Instruction;
import gov.nasa.jpf.jvm.bytecode.LDC;
import gov.nasa.jpf.jvm.bytecode.NEW;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.util.HashData;

import java.util.HashMap;
import java.util.List;
import java.util.Map;

public class ObjectIdListener extends ListenerAdapter {

       static String considerOnly = "";
       static int bound = 10;

       /**
        * Due to the fact that object construction in
        * Java is broken in two steps (NEW AND <INIT>)
        * we need to first obtain the reference and
        * then obtain all the context in the stack
        */
       public static class Status {
               private boolean processed;
               private String location;
               Status(boolean processed, String location) {
                       this.processed = processed;
                       this.location = location;
               }
               public boolean isProcessed() { return processed; }
               public void setProcessed() {
                       this.processed = true;
               }
               public String getLocation() {
                       return location;
               }
       }
      Map<Integer, Status> visited = new HashMap<Integer, Status>();

       public void instructionExecuted(JVM jvm) {

               ThreadInfo thread = jvm.getCurrentThread();
               Instruction insn = jvm.getLastInstruction();

               if (insn == null) return;

               if (insn instanceof NEW) {

                       NEW newins = (NEW) insn;
                       MethodInfo mi = newins.getMethodInfo();
                       ClassInfo parent = mi.getClassInfo();
                       if (!parent.getName().contains(considerOnly)) {
                               return;
                       }
                       try{
                       int objRef = thread.peek();// thread.getTopFrame().peek();
                       if(objRef == 369 || objRef == 359){
                    	   System.out.println("break;");
                       }
                       String position =  insn.getFileLocation();
//                      System.out.println(position);
                       visited.put(objRef, new Status(false, position));
//                      System.out.println("NEW " + objRef);
                       }catch(ArrayIndexOutOfBoundsException arrayOut){
                    	   // its happen when NEW instruction jump to a CLINIT
                    	   return;
                       }
               }else if(insn instanceof LDC){
            	   // I dont know what this type of intruction does
            	   // look likes it create constant object, like strings
            	   LDC newins = (LDC) insn;
                   MethodInfo mi = newins.getMethodInfo();
                   ClassInfo parent = mi.getClassInfo();
                   if (!parent.getName().contains(considerOnly)) {
                           return;
                   }                  
                   int objRef = thread.peek();// thread.getTopFrame().peek();
                   String position =  insn.getFileLocation();
//                  System.out.println(position);
                   visited.put(objRef, new Status(false, position));
//                  System.out.println("NEW " + objRef);
            	   
               } else if (insn instanceof INVOKESPECIAL) {
            	   try{
                       INVOKESPECIAL inv = (INVOKESPECIAL) insn;
                       MethodInfo mi = inv.getMethodInfo();
                       if (!mi.getName().contains("<init>")) {
                               return;
                       }
                       ClassInfo parent = mi.getClassInfo();
                       if (!parent.getName().contains(considerOnly)) {
                               return;
                       }
                       int objRef = thread.getTopFrame().peek();
                       
                       if(objRef == 342){
                    	   System.out.println("342");
                       }
                       
                       Status status = visited.get(objRef);
                       if (status == null) {
                    	   return;
                           //some object can be created inside EXECUTENATIVE or Other methods   
                    	   // throw new UnsupportedOperationException(""+ objRef);
                       } else if (status.isProcessed()) {
                               return;
                       }
                       status.setProcessed();
                       String position = status.getLocation();

//                      System.out.println("NEW @ " +  position);
                       int hash = genHash(thread.getStack(), position.hashCode(), bound);
                       ElementInfo eInfo = jvm.getHeap().get(objRef);
                      // System.out.printf("%s ==> %s\n", position, hash);
                       //System.out.println();
                    
                    //   System.out.println(objRef);
                       eInfo.setObjectIdHash(hash);
            	   }catch(ArrayIndexOutOfBoundsException arrayOut){
            		   return;
            	   }catch(Exception e){
            		   
            	   }
               }

       }

       private int genHash(List<StackFrame> stack, int positionHash, int bound) {
//              System.out.print("HD =>>> ");
               HashData hdata = new HashData();
               for (int i = 0; i < stack.size() && bound > 0; i++, bound--) {
                       StackFrame frame = stack.get(i);
                       frame.objectIdHash(hdata);
               }
               // hash code for this object
//              System.out.println(positionHash + " ");
               hdata.add(positionHash);
               return hdata.getValue();
       }
       
       
       public void searchStarted(Search search) {
   		super.searchStarted(search);
   		String s = search.getVM().getMainClassInfo().getPackageName();
   		int dot = s.indexOf(".");
   		if (dot == -1 /* dot not found */) {
   			considerOnly = s;
   		} else {
   			considerOnly = s.substring(0, dot);
   		}
       }
}